WithoutK-PatternSynonyms2.agda:13,14-17
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  x ≟ x₁
  x ≟ x₁
Possible reason why unification failed:
  Cannot eliminate reflexive equation x = x of type A because K has
  been disabled.
when checking that the pattern r x has type x ≡ x
